Theorema`Common`PRFOBJ$[Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`initialProofSituation, {}, {{Theorema`Common`FML$[{"ID:978540590", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb"}, Theorema`Language`Implies$TM[Theorema`Knowledge`isSurjective$TM[ Theorema`Knowledge`SmallCircle$TM[Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM], Theorema`Knowledge`X$TM, Theorema`Knowledge`Z$TM], Theorema`Knowledge`isSurjective$TM[ Theorema`Knowledge`v$TM, Theorema`Knowledge`Y$TM, Theorema`Knowledge`Z$TM]], "v \[SmallCircle] u surjective"], Theorema`Common`FML$[{"ID:112294143", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`a$TM], Theorema`Knowledge`X$TM]], True, Theorema`Language`Element$TM[Theorema`Knowledge`u$TM[ Theorema`Language`VAR$[Theorema`Knowledge`a$TM]], Theorema`Knowledge`Y$TM]], "u:X\[RightArrow]Y"]}}, "OriginalPS"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`implGoalDirect, {{Theorema`Common`FML$[{"ID:978540590", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb"}, Theorema`Language`Implies$TM[Theorema`Knowledge`isSurjective$TM[ Theorema`Knowledge`SmallCircle$TM[Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM], Theorema`Knowledge`X$TM, Theorema`Knowledge`Z$TM], Theorema`Knowledge`isSurjective$TM[ Theorema`Knowledge`v$TM, Theorema`Knowledge`Y$TM, Theorema`Knowledge`Z$TM]], "v \[SmallCircle] u surjective"]}}, {{Theorema`Common`FML$[{"ID:formula1824", "Source:none"}, Theorema`Knowledge`isSurjective$TM[Theorema`Knowledge`SmallCircle$TM[ Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM], Theorema`Knowledge`X$TM, Theorema`Knowledge`Z$TM], "A\[NumberSign]1"], Theorema`Common`FML$[{"ID:formula1825", "Source:none"}, Theorema`Knowledge`isSurjective$TM[Theorema`Knowledge`v$TM, Theorema`Knowledge`Y$TM, Theorema`Knowledge`Z$TM], "G\[NumberSign]2"]}}, "Theorema`Provers`implGoalDirect$72019"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`expandDef, {{Theorema`Common`FML$[{"ID:formula1825", "Source:none"}, Theorema`Knowledge`isSurjective$TM[Theorema`Knowledge`v$TM, Theorema`Knowledge`Y$TM, Theorema`Knowledge`Z$TM], "G\[NumberSign]2"]}, {Theorema`Common`FML$[{"ID:formula1824", "Source:none"}, Theorema`Knowledge`isSurjective$TM[ Theorema`Knowledge`SmallCircle$TM[Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM], Theorema`Knowledge`X$TM, Theorema`Knowledge`Z$TM], "A\[NumberSign]1"]}}, {{Theorema`Common`FML$[{"ID:formula1882", "Source:none"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`b$TM], Theorema`Knowledge`Z$TM]], True, Theorema`Language`Exists$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`a$TM], Theorema`Knowledge`Y$TM]], True, Theorema`Language`Equal$TM[Theorema`Knowledge`v$TM[ Theorema`Language`VAR$[Theorema`Knowledge`a$TM]], Theorema`Language`VAR$[Theorema`Knowledge`b$TM]]]], "G\[NumberSign]33"]}, {Theorema`Common`FML$[{"ID:formula1883", "Source:none"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`b$TM], Theorema`Knowledge`Z$TM]], True, Theorema`Language`Exists$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`a$TM], Theorema`Knowledge`X$TM]], True, Theorema`Language`Equal$TM[Theorema`Knowledge`SmallCircle$TM[ Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM][ Theorema`Language`VAR$[Theorema`Knowledge`a$TM]], Theorema`Language`VAR$[Theorema`Knowledge`b$TM]]]], "A\[NumberSign]34"]}}, "Theorema`Provers`expandDef$73490", "defCond" -> False, "usedDefs" -> {{Theorema`Common`FML$[{"ID:794877354", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`f$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]], True, Theorema`Language`IffDef$TM[ Theorema`Knowledge`isSurjective$TM[Theorema`Language`VAR$[ Theorema`Knowledge`f$TM], Theorema`Language`VAR$[ Theorema`Knowledge`A$TM], Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]], Theorema`Language`Forall$TM[ Theorema`Language`RNG$[Theorema`Language`SETRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`b$TM], Theorema`Language`VAR$[Theorema`Knowledge`B$TM]]], True, Theorema`Language`Exists$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`a$TM], Theorema`Language`VAR$[ Theorema`Knowledge`A$TM]]], True, Theorema`Language`Equal$TM[ Theorema`Language`VAR$[Theorema`Knowledge`f$TM][ Theorema`Language`VAR$[Theorema`Knowledge`a$TM]], Theorema`Language`VAR$[Theorema`Knowledge`b$TM]]]]]], "surjective"]}, {Theorema`Common`FML$[{"ID:794877354", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`f$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]], True, Theorema`Language`IffDef$TM[ Theorema`Knowledge`isSurjective$TM[Theorema`Language`VAR$[ Theorema`Knowledge`f$TM], Theorema`Language`VAR$[ Theorema`Knowledge`A$TM], Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]], Theorema`Language`Forall$TM[ Theorema`Language`RNG$[Theorema`Language`SETRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`b$TM], Theorema`Language`VAR$[Theorema`Knowledge`B$TM]]], True, Theorema`Language`Exists$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`a$TM], Theorema`Language`VAR$[ Theorema`Knowledge`A$TM]]], True, Theorema`Language`Equal$TM[ Theorema`Language`VAR$[Theorema`Knowledge`f$TM][ Theorema`Language`VAR$[Theorema`Knowledge`a$TM]], Theorema`Language`VAR$[Theorema`Knowledge`b$TM]]]]]], "surjective"]}}], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`forallGoal, {{Theorema`Common`FML$[{"ID:formula1882", "Source:none"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`b$TM], Theorema`Knowledge`Z$TM]], True, Theorema`Language`Exists$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`a$TM], Theorema`Knowledge`Y$TM]], True, Theorema`Language`Equal$TM[Theorema`Knowledge`v$TM[ Theorema`Language`VAR$[Theorema`Knowledge`a$TM]], Theorema`Language`VAR$[Theorema`Knowledge`b$TM]]]], "G\[NumberSign]33"]}}, {{Theorema`Common`FML$[{"ID:formula1895", "Source:none"}, Theorema`Language`Exists$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`a$TM], Theorema`Knowledge`Y$TM]], True, Theorema`Language`Equal$TM[Theorema`Knowledge`v$TM[ Theorema`Language`VAR$[Theorema`Knowledge`a$TM]], Theorema`Language`FIX$[Theorema`Knowledge`b$TM, 0]]], "G\[NumberSign]41"], Theorema`Common`FML$[{"ID:formula1896", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`b$TM, 0], Theorema`Knowledge`Z$TM], "A\[NumberSign]42"]}}, "Theorema`Provers`forallGoal$73845", "abf" -> {Theorema`Language`FIX$[Theorema`Knowledge`b$TM, 0]}], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`existsGoal, {{Theorema`Common`FML$[{"ID:formula1895", "Source:none"}, Theorema`Language`Exists$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`a$TM], Theorema`Knowledge`Y$TM]], True, Theorema`Language`Equal$TM[Theorema`Knowledge`v$TM[ Theorema`Language`VAR$[Theorema`Knowledge`a$TM]], Theorema`Language`FIX$[Theorema`Knowledge`b$TM, 0]]], "G\[NumberSign]41"]}}, {{Theorema`Common`FML$[{"ID:formula1912", "Source:none"}, Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`META$[Theorema`Knowledge`a$TM, 0, {Theorema`Language`FIX$[Theorema`Knowledge`b$TM, 0]}], Theorema`Knowledge`Y$TM], Theorema`Language`Equal$TM[ Theorema`Knowledge`v$TM[Theorema`Language`META$[ Theorema`Knowledge`a$TM, 0, {Theorema`Language`FIX$[ Theorema`Knowledge`b$TM, 0]}]], Theorema`Language`FIX$[ Theorema`Knowledge`b$TM, 0]]], "G\[NumberSign]53"]}}, "Theorema`Provers`existsGoal$74258", "meta" -> {Theorema`Language`META$[Theorema`Knowledge`a$TM, 0, {Theorema`Language`FIX$[Theorema`Knowledge`b$TM, 0]}]}], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`knowledgeRewriting, {{Theorema`Common`FML$[{"ID:formula1896", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`b$TM, 0], Theorema`Knowledge`Z$TM], "A\[NumberSign]42"], Theorema`Common`FML$[{"ID:formula1883", "Source:none"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`b$TM], Theorema`Knowledge`Z$TM]], True, Theorema`Language`Exists$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`a$TM], Theorema`Knowledge`X$TM]], True, Theorema`Language`Equal$TM[Theorema`Knowledge`SmallCircle$TM[ Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM][ Theorema`Language`VAR$[Theorema`Knowledge`a$TM]], Theorema`Language`VAR$[Theorema`Knowledge`b$TM]]]], "A\[NumberSign]34"]}}, {{Theorema`Common`FML$[{"ID:formula1940", "Source:none"}, Theorema`Language`Exists$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`a$TM], Theorema`Knowledge`X$TM]], True, Theorema`Language`Equal$TM[Theorema`Knowledge`SmallCircle$TM[ Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM][ Theorema`Language`VAR$[Theorema`Knowledge`a$TM]], Theorema`Language`FIX$[Theorema`Knowledge`b$TM, 0]]], "A\[NumberSign]73"]}}, "Theorema`Provers`knowledgeRewriting$75018"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`existsKB, {{Theorema`Common`FML$[{"ID:formula1940", "Source:none"}, Theorema`Language`Exists$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`a$TM], Theorema`Knowledge`X$TM]], True, Theorema`Language`Equal$TM[Theorema`Knowledge`SmallCircle$TM[ Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM][ Theorema`Language`VAR$[Theorema`Knowledge`a$TM]], Theorema`Language`FIX$[Theorema`Knowledge`b$TM, 0]]], "A\[NumberSign]73"]}}, {{Theorema`Common`FML$[{"ID:formula1959", "Source:none"}, Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`a$TM, 0], Theorema`Knowledge`X$TM], "A\[NumberSign]87"], Theorema`Common`FML$[{"ID:formula1960", "Source:none"}, Theorema`Language`Equal$TM[Theorema`Knowledge`SmallCircle$TM[ Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM][ Theorema`Language`FIX$[Theorema`Knowledge`a$TM, 0]], Theorema`Language`FIX$[Theorema`Knowledge`b$TM, 0]], "A\[NumberSign]88"]}}, "Theorema`Provers`existsKB$75588", "abf" -> {Theorema`Language`FIX$[Theorema`Knowledge`a$TM, 0]}], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`elementarySubstitution, {{Theorema`Common`FML$[{"ID:formula1912", "Source:none"}, Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`META$[Theorema`Knowledge`a$TM, 0, { Theorema`Language`FIX$[Theorema`Knowledge`b$TM, 0]}], Theorema`Knowledge`Y$TM], Theorema`Language`Equal$TM[ Theorema`Knowledge`v$TM[Theorema`Language`META$[ Theorema`Knowledge`a$TM, 0, {Theorema`Language`FIX$[ Theorema`Knowledge`b$TM, 0]}]], Theorema`Language`FIX$[ Theorema`Knowledge`b$TM, 0]]], "G\[NumberSign]53"], Theorema`Common`FML$[{"ID:formula1960", "Source:none"}, Theorema`Language`Equal$TM[Theorema`Knowledge`SmallCircle$TM[ Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM][ Theorema`Language`FIX$[Theorema`Knowledge`a$TM, 0]], Theorema`Language`FIX$[Theorema`Knowledge`b$TM, 0]], "A\[NumberSign]88"]}}, {{Theorema`Common`FML$[{"ID:formula1984", "Source:none"}, Theorema`Language`And$TM[ Theorema`Language`Element$TM[Theorema`Language`META$[ Theorema`Knowledge`a$TM, 0, {Theorema`Knowledge`SmallCircle$TM[ Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM][ Theorema`Language`FIX$[Theorema`Knowledge`a$TM, 0]]}], Theorema`Knowledge`Y$TM], Theorema`Language`Equal$TM[ Theorema`Knowledge`v$TM[Theorema`Language`META$[ Theorema`Knowledge`a$TM, 0, {Theorema`Knowledge`SmallCircle$TM[Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM][Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0]]}]], Theorema`Knowledge`SmallCircle$TM[Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM][Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0]]]], "G\[NumberSign]108"]}}, "Theorema`Provers`elementarySubstitution$76238", "goalRewrite" -> True, "usedSubst" -> {{Theorema`Common`FML$[{"ID:formula1960", "Source:none"}, Theorema`Language`Equal$TM[Theorema`Knowledge`SmallCircle$TM[ Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM][ Theorema`Language`FIX$[Theorema`Knowledge`a$TM, 0]], Theorema`Language`FIX$[Theorema`Knowledge`b$TM, 0]], "A\[NumberSign]88"]}, {Theorema`Common`FML$[{"ID:formula1960", "Source:none"}, Theorema`Language`Equal$TM[ Theorema`Knowledge`SmallCircle$TM[Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM][Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0]], Theorema`Language`FIX$[ Theorema`Knowledge`b$TM, 0]], "A\[NumberSign]88"]}}], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`knowledgeRewriting, {{Theorema`Common`FML$[{"ID:formula1959", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0], Theorema`Knowledge`X$TM], "A\[NumberSign]87"], Theorema`Common`FML$[{"ID:112294143", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb"}\ , Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`a$TM], Theorema`Knowledge`X$TM]], True, Theorema`Language`Element$TM[Theorema`Knowledge`u$TM[ Theorema`Language`VAR$[Theorema`Knowledge`a$TM]], Theorema`Knowledge`Y$TM]], "u:X\[RightArrow]Y"]}}, {{Theorema`Common`FML$[{"ID:formula2032", "Source:none"}, Theorema`Language`Element$TM[Theorema`Knowledge`u$TM[ Theorema`Language`FIX$[Theorema`Knowledge`a$TM, 0]], Theorema`Knowledge`Y$TM], "A\[NumberSign]148"]}}, "Theorema`Provers`knowledgeRewriting$77148"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`expandDef, {{Theorema`Common`FML$[ {"ID:formula1984", "Source:none"}, Theorema`Language`And$TM[ Theorema`Language`Element$TM[Theorema`Language`META$[ Theorema`Knowledge`a$TM, 0, {Theorema`Knowledge`SmallCircle$TM[Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM][Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0]]}], Theorema`Knowledge`Y$TM], Theorema`Language`Equal$TM[Theorema`Knowledge`v$TM[ Theorema`Language`META$[Theorema`Knowledge`a$TM, 0, {Theorema`Knowledge`SmallCircle$TM[Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM][Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0]]}]], Theorema`Knowledge`SmallCircle$TM[Theorema`Knowledge`v$TM, Theorema`Knowledge`u$TM][Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0]]]], "G\[NumberSign]108"]}}, {{Theorema`Common`FML$[{"ID:formula2219", "Source:none"}, Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`META$[Theorema`Knowledge`a$TM, 0, {Theorema`Knowledge`v$TM[Theorema`Knowledge`u$TM[ Theorema`Language`FIX$[Theorema`Knowledge`a$TM, 0]]]}], Theorema`Knowledge`Y$TM], Theorema`Language`Equal$TM[ Theorema`Knowledge`v$TM[Theorema`Language`META$[ Theorema`Knowledge`a$TM, 0, {Theorema`Knowledge`v$TM[ Theorema`Knowledge`u$TM[Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0]]]}]], Theorema`Knowledge`v$TM[Theorema`Knowledge`u$TM[ Theorema`Language`FIX$[Theorema`Knowledge`a$TM, 0]]]]], "G\[NumberSign]314"]}}, "Theorema`Provers`expandDef$80387", "defCond" -> False, "usedDefs" -> {{Theorema`Common`FML$[{ "ID:1636230891", "Source:/home/wwindste/Publications/Talks/20\ 14-10-WTC/Talk.nb"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`f$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`g$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]]], True, Theorema`Language`EqualDef$TM[ Theorema`Knowledge`SmallCircle$TM[Theorema`Language`VAR$[ Theorema`Knowledge`g$TM], Theorema`Language`VAR$[ Theorema`Knowledge`f$TM]][Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]], Theorema`Language`VAR$[ Theorema`Knowledge`g$TM][Theorema`Language`VAR$[ Theorema`Knowledge`f$TM][Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]]]]], "composition"]}, {Theorema`Common`FML$[{"ID:1636230891", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb\ "}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`f$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`g$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]]], True, Theorema`Language`EqualDef$TM[ Theorema`Knowledge`SmallCircle$TM[Theorema`Language`VAR$[ Theorema`Knowledge`g$TM], Theorema`Language`VAR$[ Theorema`Knowledge`f$TM]][Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]], Theorema`Language`VAR$[ Theorema`Knowledge`g$TM][Theorema`Language`VAR$[ Theorema`Knowledge`f$TM][Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]]]]], "composition"]}, {Theorema`Common`FML$[{"ID:1636230891", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb\ "}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`f$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`g$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]]], True, Theorema`Language`EqualDef$TM[ Theorema`Knowledge`SmallCircle$TM[Theorema`Language`VAR$[ Theorema`Knowledge`g$TM], Theorema`Language`VAR$[ Theorema`Knowledge`f$TM]][Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]], Theorema`Language`VAR$[ Theorema`Knowledge`g$TM][Theorema`Language`VAR$[ Theorema`Knowledge`f$TM][Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]]]]], "composition"]}, {Theorema`Common`FML$[{"ID:1636230891", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb\ "}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`f$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`g$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]]], True, Theorema`Language`EqualDef$TM[ Theorema`Knowledge`SmallCircle$TM[Theorema`Language`VAR$[ Theorema`Knowledge`g$TM], Theorema`Language`VAR$[ Theorema`Knowledge`f$TM]][Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]], Theorema`Language`VAR$[ Theorema`Knowledge`g$TM][Theorema`Language`VAR$[ Theorema`Knowledge`f$TM][Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]]]]], "composition"]}, {Theorema`Common`FML$[{"ID:1636230891", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/Talk.nb\ "}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`f$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`g$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]]], True, Theorema`Language`EqualDef$TM[ Theorema`Knowledge`SmallCircle$TM[Theorema`Language`VAR$[ Theorema`Knowledge`g$TM], Theorema`Language`VAR$[ Theorema`Knowledge`f$TM]][Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]], Theorema`Language`VAR$[ Theorema`Knowledge`g$TM][Theorema`Language`VAR$[ Theorema`Knowledge`f$TM][Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]]]]], "composition"]}}], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`solveMetaUnification, {{Theorema`Common`FML$[{"ID:formula2219", "Source:none"}, Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`META$[Theorema`Knowledge`a$TM, 0, {Theorema`Knowledge`v$TM[Theorema`Knowledge`u$TM[ Theorema`Language`FIX$[Theorema`Knowledge`a$TM, 0]]]}], Theorema`Knowledge`Y$TM], Theorema`Language`Equal$TM[ Theorema`Knowledge`v$TM[Theorema`Language`META$[ Theorema`Knowledge`a$TM, 0, {Theorema`Knowledge`v$TM[ Theorema`Knowledge`u$TM[Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0]]]}]], Theorema`Knowledge`v$TM[Theorema`Knowledge`u$TM[ Theorema`Language`FIX$[Theorema`Knowledge`a$TM, 0]]]]], "G\[NumberSign]314"]}}, {{Theorema`Common`FML$[{ "ID:formula2397", "Source:none"}, Theorema`Language`Element$TM[Theorema`Knowledge`u$TM[ Theorema`Language`FIX$[Theorema`Knowledge`a$TM, 0]], Theorema`Knowledge`Y$TM], "G\[NumberSign]477", "origForm" -> Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Knowledge`u$TM[Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0]], Theorema`Knowledge`Y$TM], Theorema`Language`Equal$TM[Theorema`Knowledge`v$TM[ Theorema`Knowledge`u$TM[Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0]]], Theorema`Knowledge`v$TM[ Theorema`Knowledge`u$TM[Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0]]]]]]}}, "Theorema`Provers`solveMetaUnification$84637", "instantiation" -> {{Theorema`Language`META$[Theorema`Knowledge`a$TM, 0, {Theorema`Knowledge`v$TM[Theorema`Knowledge`u$TM[ Theorema`Language`FIX$[Theorema`Knowledge`a$TM, 0]]]}] -> Theorema`Knowledge`u$TM[Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0]]}}], Theorema`Provers`Common`Private`TERMINALNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`goalInKB, {{Theorema`Common`FML$[ {"ID:formula2397", "Source:none"}, Theorema`Language`Element$TM[Theorema`Knowledge`u$TM[ Theorema`Language`FIX$[Theorema`Knowledge`a$TM, 0]], Theorema`Knowledge`Y$TM], "G\[NumberSign]477", "origForm" -> Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Knowledge`u$TM[Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0]], Theorema`Knowledge`Y$TM], Theorema`Language`Equal$TM[Theorema`Knowledge`v$TM[ Theorema`Knowledge`u$TM[Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0]]], Theorema`Knowledge`v$TM[ Theorema`Knowledge`u$TM[Theorema`Language`FIX$[ Theorema`Knowledge`a$TM, 0]]]]]], Theorema`Common`FML$[ {"ID:formula2032", "Source:none"}, Theorema`Language`Element$TM[Theorema`Knowledge`u$TM[ Theorema`Language`FIX$[Theorema`Knowledge`a$TM, 0]], Theorema`Knowledge`Y$TM], "A\[NumberSign]148"]}}, {}, "Theorema`Provers`goalInKB$84642"], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved]