[STATEMENT]
lemma (in infinite_coin_toss_space) pseudo_proj_False_neq_True:
  shows "pseudo_proj_False n w \<noteq> pseudo_proj_True n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pseudo_proj_False n w \<noteq> pseudo_proj_True n w
[PROOF STEP]
proof (rule diff_streams_if, intro exI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pseudo_proj_False n w !! ?n2 \<noteq> pseudo_proj_True n w !! ?n2
[PROOF STEP]
have "snth (pseudo_proj_False n w) n = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pseudo_proj_False n w !! n = False
[PROOF STEP]
unfolding pseudo_proj_False_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((stake n w @ [False]) @- sconst True) !! n = False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pseudo_proj_False n w !! n = False

goal (1 subgoal):
 1. pseudo_proj_False n w !! ?n2 \<noteq> pseudo_proj_True n w !! ?n2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pseudo_proj_False n w !! n = False

goal (1 subgoal):
 1. pseudo_proj_False n w !! ?n2 \<noteq> pseudo_proj_True n w !! ?n2
[PROOF STEP]
have "snth (pseudo_proj_True n w) n = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pseudo_proj_True n w !! n = True
[PROOF STEP]
unfolding pseudo_proj_True_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (stake n w @- sconst True) !! n = True
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pseudo_proj_True n w !! n = True

goal (1 subgoal):
 1. pseudo_proj_False n w !! ?n2 \<noteq> pseudo_proj_True n w !! ?n2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pseudo_proj_False n w !! n = False
pseudo_proj_True n w !! n = True
[PROOF STEP]
show "snth (pseudo_proj_False n w) n \<noteq> snth (pseudo_proj_True n w) n"
[PROOF STATE]
proof (prove)
using this:
pseudo_proj_False n w !! n = False
pseudo_proj_True n w !! n = True

goal (1 subgoal):
 1. pseudo_proj_False n w !! n \<noteq> pseudo_proj_True n w !! n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pseudo_proj_False n w !! n \<noteq> pseudo_proj_True n w !! n

goal:
No subgoals!
[PROOF STEP]
qed